$\forall$$T$:Type$_{\mbox{\scriptsize i}}$, $S$:($\mathbb{N}\rightarrow$($\mathbb{N}\rightarrow$$T$)$\rightarrow$Prop$_{\mbox{\scriptsize i'}}$).
\\[0ex]($\forall$$i$:$\mathbb{N}$. generic\{i:l\}($T$; $x$.$S$($i$,$x$))) $\Rightarrow$ generic\{i:l\}($T$; $x$.($\forall$$i$:$\mathbb{N}$. $S$($i$,$x$)))